<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>seL4 2.0.0 | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/releases/sel4">
              <span property="name"><b>seL4 releases</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">seL4 2.0.0</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">
















</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="introducing-sel4-200">Introducing seL4 2.0.0</h1>

<p>Version 2.0.0 introduces more consistent terminology to manual and code,
as well as API and performance improvements, including to seL4’s
formally verified ARMv6 version.</p>

<p>We clarified the notion of signals and notifications vs IPC, and added a
new feature to the seL4 API that allows user programs to receive
notifications while waiting for IPC messages. You can now also poll
notification objects. Both of these changes are aimed at simplifying
user-level interaction with interrupts.</p>

<p>In addition to the new features, seL4 has become even faster than it was
before, esp. in scheduling threads.</p>

<p>The new features and performance improvements are available on all
supported platforms, and are formally verified to full sel4 standards.
We have also switched our release process to semantic versioning, so
it’s easy to tell which seL4 releases are binary-compatible,
source-compatible, or will require updates to user-level code.</p>

<h1 id="terminology-changes">Terminology Changes</h1>

<h2 id="ipc-vs-notifications">IPC vs Notifications</h2>

<p>The old terminology of “synchronous IPC” vs “asynchronous IPC” was
confusing and misleading. We changed this to reflect the fact that IPC
in seL4 is always synchronous and is simply referred to as “IPC”, which
is enabled by “endpoint” objects. The receive operation is now more
appropriately called “receive”.</p>

<p>What used to be called incorrectly “asynchronous IPC” is now called
Notifications, enabled by “notification” objects. Notifications are not
a form of message passing, but arrays of binary semaphores, and the new
terminology describes this better. The operations on them are
consequently called “signal” and “wait”</p>

<h1 id="new-features">New Features</h1>

<h2 id="notification-binding">Notification binding</h2>

<p>A notification can be bound to a thread and is referred to as the
thread’s bound notification object. This is a 1:1 relationship. Whenever
a thread waits for an IPC on an endpoint, it will receive any signals
sent to its bound notification object, with the signal flags converted
into a single-word message.</p>

<p>Threads can also explicitly wait for signals by waiting on the
notification object itself.</p>

<p>For more details, see the 2.0.0 manual</p>

<h1 id="implementation-improvements">Implementation improvements</h1>

<ul>
  <li>introduces the bitfield scheduler: faster scheduler (Was linear in
    the</li>
</ul>

<p>number of runnable threads, now log n)</p>

<ul>
  <li>improved benchmarking macros: can now specify multiple
      benchmarking</li>
</ul>

<p>tracepoints at once added
<code class="language-plaintext highlighter-rouge">CONFIG_RELEASE_PRINTF</code> in addition to <code class="language-plaintext highlighter-rouge">CONFIG_DEBUG</code> and <code class="language-plaintext highlighter-rouge">CONFIG_RELEASE</code>, which
enables printf in a release build</p>

<h1 id="api-changes">API Changes</h1>

<ul>
  <li><code class="language-plaintext highlighter-rouge">seL4_Recv</code> replaces <code class="language-plaintext highlighter-rouge">seL4_Wait</code> on endpoints</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_Wait</code> is now only used on notification objects</li>
  <li>Async endpoint -&gt; notification object</li>
  <li>sync endpoint -&gt; endpoint</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_Recv</code> on an endpoint may now return signals sent to a
    thread’s</li>
</ul>

<p>bound notification object.</p>

<h2 id="api-additions">API Additions</h2>

<ul>
  <li><code class="language-plaintext highlighter-rouge">seL4_NotificationObject</code> replaces deprecated
    <code class="language-plaintext highlighter-rouge">seL4_AsyncEndpointObject</code></li>
  <li><code class="language-plaintext highlighter-rouge">seL4_NotificationBits</code> size in bits of a notification object</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_IRQHandler_SetNotification</code> replaces deprecated
    <code class="language-plaintext highlighter-rouge">seL4_IRQHandler_SetEndpoint</code></li>
  <li><code class="language-plaintext highlighter-rouge">seL4_Recv</code> replaces <code class="language-plaintext highlighter-rouge">seL4_Wait</code> for endpoints</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_Wait</code> used on notifications</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_NBRecv</code> non-blocking (polling) receive on an endpoint,
    which fails</li>
</ul>

<p>if there is no message waiting. Opposite of <code class="language-plaintext highlighter-rouge">NBSend</code> (which silently
fails if there is no receiver waiting)</p>
<ul>
  <li><code class="language-plaintext highlighter-rouge">seL4_Poll</code> collects any
signals from a notification objects, returns zero if there are none</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_Signal</code> replaces deprecated <code class="language-plaintext highlighter-rouge">seL4_Notify</code></li>
  <li><code class="language-plaintext highlighter-rouge">seL4_TCB_BindNotification</code> bind a notification to a tcb</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_TCB_UnbindNotification</code> unbind a notification from a tcb</li>
</ul>

<h2 id="deprecations">Deprecations</h2>

<ul>
  <li><code class="language-plaintext highlighter-rouge">seL4_AsyncEndpointObject</code></li>
  <li><code class="language-plaintext highlighter-rouge">seL4_Notify</code></li>
  <li><code class="language-plaintext highlighter-rouge">seL4_IRQHandler_SetEndpoint</code></li>
</ul>

<h1 id="note-on-syscall-names">Note on Syscall names</h1>

<p>Logically there are only two operations on capabilities, send and
receive, which can take opcodes specifying sup-operations. For example,
the Notification operations Signal and Wait are mapped to Send and
Receive, respectively. For efficiency reasons, many kernel objects use
separate kernel entry points for their operations. You must not rely on
either, as this can change at any time. Instead, always use the
object-specific wrapper functions.</p>

<h1 id="user-level-repositories">User-level repositories</h1>

<p>To simply repository management we have merged many of our user level
library repositories. To see the changes please compare 1.0.4.xml and
2.0.x.xml in <a href="https://github.com/seL4/seL4test-manifest">https://github.com/seL4/seL4test-manifest</a></p>

<h1 id="upgrade-notes">Upgrade notes</h1>

<p>Calls to <code class="language-plaintext highlighter-rouge">seL4_Wait</code> no longer return a <code class="language-plaintext highlighter-rouge">seL4_MessageInfo_t</code>
as <code class="language-plaintext highlighter-rouge">seL4_Wait</code> is intended to be used on notification objects.
Calls to the prior version of <code class="language-plaintext highlighter-rouge">seL4_Wait</code> need to be replaced with
<code class="language-plaintext highlighter-rouge">seL4_Recv</code>.</p>

<p>If you don’t want to upgrade yet - don’t worry. Both the
sel4test-manifest and verification manifest repositories have manifests
titled 1.0.4.xml which point to the tips of the previously released
repositories before today. All library repositories have a branch called
‘1.0.x-compatible’ which are compatible with the 1.0.4 kernel.</p>

<p>Note that to use the new merged repositories, you must upgrade to 2.0.0.</p>

<h1 id="full-changelog">Full changelog</h1>

<p>Use git log 1.0.4..2.0.0 in <a href="https://github.com/seL4/seL4">https://github.com/seL4/seL4</a></p>

<h1 id="more-details">More details</h1>

<p>See the <a href="http://sel4.systems/Info/Docs/seL4-manual-2.0.0.pdf">2.0.0
manual</a>
included in the release for detailed descriptions of the new features.
Or ask on this mailing list!</p>


  </div>







  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> seL4 </h2> 
        <li>
          
          <a style="" class="" href="/projects/sel4/">
            Documentation homepage
          </a>
        </li>




        <li>
          
          <a style="" class="" href="/projects/sel4/status.html">
            Status
          </a>
        </li>














    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/seL4/sel4">
            sel4
          </a>
        </li>









<h3>Releases</h3>

    
      <li>
        <a style="" href="/releases/sel4/13.0.0.html">
          seL4 13.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-13.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/12.1.0.html">
          seL4 12.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-12.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/12.0.0.html">
          seL4 12.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-12.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/11.0.0.html">
          seL4 11.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-11.0.0.pdf">manual</a>)
      </li>

    


    


    
      <li>
        <a style="" href="/releases/sel4/10.1.1.html">
          seL4 10.1.1
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/10.1.0.html">
          seL4 10.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-10.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/10.0.0.html">
          seL4 10.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-10.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/9.0.1.html">
          seL4 9.0.1
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf">manual</a>)
      </li>

    


    


    
      <li>
        <a style="" href="/releases/sel4/9.0.0.html">
          seL4 9.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-9.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/8.0.0.html">
          seL4 8.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-8.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/7.0.0.html">
          seL4 7.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-7.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/6.0.0.html">
          seL4 6.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-6.0.0.pdf">manual</a>)
      </li>

    


    


    
      <li>
        <a style="" href="/releases/sel4/5.2.0.html">
          seL4 5.2.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-5.2.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/5.1.0.html">
          seL4 5.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-5.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/5.0.0.html">
          seL4 5.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-5.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/4.0.0.html">
          seL4 4.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.2.0.html">
          seL4 3.2.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.2.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.1.0.html">
          seL4 3.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.0.1.html">
          seL4 3.0.1
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.0.1.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.0.0.html">
          seL4 3.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/2.1.0.html">
          seL4 2.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-2.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style=" font-weight: bold; " href="/releases/sel4/2.0.0.html">
          seL4 2.0.0
        </a> (<a style=" font-weight: bold; " href="http://sel4.systems/Info/Docs/seL4-manual-2.0.0.pdf">manual</a>)
      </li>

    


    


    










    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/content_collections/_releases/sel4/2.0.0.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/content_collections/_releases/sel4/2.0.0.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
